Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar18/AProVESLASHJFP

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

nats_active -> add_active₁(zeros_active)
hd_active₁(x) -> hd₁(x)
zeros_active -> cons₂(0, zeros)
tl_active₁(x) -> tl₁(x)
incr_active₁(cons₂(x, y)) -> cons₂(s₁(x), incr₁(y))
mark₁(nats) -> nats_active
add_active₁(cons₂(x, y)) -> incr_active₁(cons₂(x, add₁(y)))
mark₁(zeros) -> zeros_active
hd_active₁(cons₂(x, y)) -> mark₁(x)
mark₁(incr₁(x)) -> incr_active₁(mark₁(x))
tl_active₁(cons₂(x, y)) -> mark₁(y)
mark₁(add₁(x)) -> add_active₁(mark₁(x))
nats_active -> nats
mark₁(hd₁(x)) -> hd_active₁(mark₁(x))
zeros_active -> zeros
mark₁(tl₁(x)) -> tl_active₁(mark₁(x))
incr_active₁(x) -> incr₁(x)
mark₁(0) -> 0
add_active₁(x) -> add₁(x)
mark₁(s₁(x)) -> s₁(x)
mark₁(cons₂(x, y)) -> cons₂(x, y)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

nats_active -> add_active₁(zeros_active)
hd_active₁(x) -> hd₁(x)
zeros_active -> cons₂(0, zeros)
tl_active₁(x) -> tl₁(x)
incr_active₁(cons₂(x, y)) -> cons₂(s₁(x), incr₁(y))
mark₁(nats) -> nats_active
add_active₁(cons₂(x, y)) -> incr_active₁(cons₂(x, add₁(y)))
mark₁(zeros) -> zeros_active
hd_active₁(cons₂(x, y)) -> mark₁(x)
mark₁(incr₁(x)) -> incr_active₁(mark₁(x))
tl_active₁(cons₂(x, y)) -> mark₁(y)
mark₁(add₁(x)) -> add_active₁(mark₁(x))
nats_active -> nats
mark₁(hd₁(x)) -> hd_active₁(mark₁(x))
zeros_active -> zeros
mark₁(tl₁(x)) -> tl_active₁(mark₁(x))
incr_active₁(x) -> incr₁(x)
mark₁(0) -> 0
add_active₁(x) -> add₁(x)
mark₁(s₁(x)) -> s₁(x)
mark₁(cons₂(x, y)) -> cons₂(x, y)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK₁(nats) -> NATS_ACTIVE
MARK₁(tl₁(x)) -> MARK₁(x)
ADD_ACTIVE₁(cons₂(x, y)) -> INCR_ACTIVE₁(cons₂(x, add₁(y)))
MARK₁(tl₁(x)) -> TL_ACTIVE₁(mark₁(x))
MARK₁(add₁(x)) -> MARK₁(x)
HD_ACTIVE₁(cons₂(x, y)) -> MARK₁(x)
MARK₁(zeros) -> ZEROS_ACTIVE
MARK₁(incr₁(x)) -> INCR_ACTIVE₁(mark₁(x))
MARK₁(add₁(x)) -> ADD_ACTIVE₁(mark₁(x))
MARK₁(hd₁(x)) -> HD_ACTIVE₁(mark₁(x))
NATS_ACTIVE -> ZEROS_ACTIVE
MARK₁(hd₁(x)) -> MARK₁(x)
NATS_ACTIVE -> ADD_ACTIVE₁(zeros_active)
TL_ACTIVE₁(cons₂(x, y)) -> MARK₁(y)
MARK₁(incr₁(x)) -> MARK₁(x)

The TRS R consists of the following rules:

nats_active -> add_active₁(zeros_active)
hd_active₁(x) -> hd₁(x)
zeros_active -> cons₂(0, zeros)
tl_active₁(x) -> tl₁(x)
incr_active₁(cons₂(x, y)) -> cons₂(s₁(x), incr₁(y))
mark₁(nats) -> nats_active
add_active₁(cons₂(x, y)) -> incr_active₁(cons₂(x, add₁(y)))
mark₁(zeros) -> zeros_active
hd_active₁(cons₂(x, y)) -> mark₁(x)
mark₁(incr₁(x)) -> incr_active₁(mark₁(x))
tl_active₁(cons₂(x, y)) -> mark₁(y)
mark₁(add₁(x)) -> add_active₁(mark₁(x))
nats_active -> nats
mark₁(hd₁(x)) -> hd_active₁(mark₁(x))
zeros_active -> zeros
mark₁(tl₁(x)) -> tl_active₁(mark₁(x))
incr_active₁(x) -> incr₁(x)
mark₁(0) -> 0
add_active₁(x) -> add₁(x)
mark₁(s₁(x)) -> s₁(x)
mark₁(cons₂(x, y)) -> cons₂(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK₁(nats) -> NATS_ACTIVE
MARK₁(tl₁(x)) -> MARK₁(x)
ADD_ACTIVE₁(cons₂(x, y)) -> INCR_ACTIVE₁(cons₂(x, add₁(y)))
MARK₁(tl₁(x)) -> TL_ACTIVE₁(mark₁(x))
MARK₁(add₁(x)) -> MARK₁(x)
HD_ACTIVE₁(cons₂(x, y)) -> MARK₁(x)
MARK₁(zeros) -> ZEROS_ACTIVE
MARK₁(incr₁(x)) -> INCR_ACTIVE₁(mark₁(x))
MARK₁(add₁(x)) -> ADD_ACTIVE₁(mark₁(x))
MARK₁(hd₁(x)) -> HD_ACTIVE₁(mark₁(x))
NATS_ACTIVE -> ZEROS_ACTIVE
MARK₁(hd₁(x)) -> MARK₁(x)
NATS_ACTIVE -> ADD_ACTIVE₁(zeros_active)
TL_ACTIVE₁(cons₂(x, y)) -> MARK₁(y)
MARK₁(incr₁(x)) -> MARK₁(x)

The TRS R consists of the following rules:

nats_active -> add_active₁(zeros_active)
hd_active₁(x) -> hd₁(x)
zeros_active -> cons₂(0, zeros)
tl_active₁(x) -> tl₁(x)
incr_active₁(cons₂(x, y)) -> cons₂(s₁(x), incr₁(y))
mark₁(nats) -> nats_active
add_active₁(cons₂(x, y)) -> incr_active₁(cons₂(x, add₁(y)))
mark₁(zeros) -> zeros_active
hd_active₁(cons₂(x, y)) -> mark₁(x)
mark₁(incr₁(x)) -> incr_active₁(mark₁(x))
tl_active₁(cons₂(x, y)) -> mark₁(y)
mark₁(add₁(x)) -> add_active₁(mark₁(x))
nats_active -> nats
mark₁(hd₁(x)) -> hd_active₁(mark₁(x))
zeros_active -> zeros
mark₁(tl₁(x)) -> tl_active₁(mark₁(x))
incr_active₁(x) -> incr₁(x)
mark₁(0) -> 0
add_active₁(x) -> add₁(x)
mark₁(s₁(x)) -> s₁(x)
mark₁(cons₂(x, y)) -> cons₂(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 7 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK₁(tl₁(x)) -> MARK₁(x)
MARK₁(tl₁(x)) -> TL_ACTIVE₁(mark₁(x))
MARK₁(add₁(x)) -> MARK₁(x)
HD_ACTIVE₁(cons₂(x, y)) -> MARK₁(x)
TL_ACTIVE₁(cons₂(x, y)) -> MARK₁(y)
MARK₁(hd₁(x)) -> HD_ACTIVE₁(mark₁(x))
MARK₁(incr₁(x)) -> MARK₁(x)
MARK₁(hd₁(x)) -> MARK₁(x)

The TRS R consists of the following rules:

nats_active -> add_active₁(zeros_active)
hd_active₁(x) -> hd₁(x)
zeros_active -> cons₂(0, zeros)
tl_active₁(x) -> tl₁(x)
incr_active₁(cons₂(x, y)) -> cons₂(s₁(x), incr₁(y))
mark₁(nats) -> nats_active
add_active₁(cons₂(x, y)) -> incr_active₁(cons₂(x, add₁(y)))
mark₁(zeros) -> zeros_active
hd_active₁(cons₂(x, y)) -> mark₁(x)
mark₁(incr₁(x)) -> incr_active₁(mark₁(x))
tl_active₁(cons₂(x, y)) -> mark₁(y)
mark₁(add₁(x)) -> add_active₁(mark₁(x))
nats_active -> nats
mark₁(hd₁(x)) -> hd_active₁(mark₁(x))
zeros_active -> zeros
mark₁(tl₁(x)) -> tl_active₁(mark₁(x))
incr_active₁(x) -> incr₁(x)
mark₁(0) -> 0
add_active₁(x) -> add₁(x)
mark₁(s₁(x)) -> s₁(x)
mark₁(cons₂(x, y)) -> cons₂(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.